\section{Comparison with IsaPlanner}
\label{sec:comparison}

We now compare Zeno, IsaPlanner and ACL2s in terms of their respective performance
 % by measuring the number of properties each could prove.
on a set of properties listed on
 % The set of properties we used were taken from
 a page from the IsaPlanner
 website\footnote{\url{http://dream.inf.ed.ac.uk/projects/lemmadiscovery/results/case-analysis-rippling.txt}}.
This set also appears in
 one of the IsaPlanner authors' papers\cite{caseanalysisrippling}.

Of these 87 properties Zeno could prove 82, and 2 are false, leaving 3 properties unproven. IsaPlanner could prove 47 properties, while ACL2s was able to prove 69 properties. There were no properties which ACL2s or IsaPlanner could prove and Zeno could not. There were 8 properties IsaPlanner could prove over ACL2s, and 30 which ACL2s could prove over IsaPlanner.

The longest Zeno proof took 2.084s, while most proofs took less than 0.001s, running on an Intel Core i5-650 processor. The other two tools produced proofs in similar times. An table of provable properties for each tool is in Appendix \ref{app:timings}. The Haskell code for the function definitions used to test Zeno is in Appendix \ref{app:code} and the Common LISP translation used to test ACL2s is in Appendix \ref{app:lisp}. As ACL2s functions are untyped we supplied type information in the form of proven theorems.

